Problem: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) Proof: Bounds Processor: bound: 4 enrichment: match automaton: final states: {5,4,3} transitions: 02(223) -> 224* 01(15) -> 16* 01(114) -> 115* 01(86) -> 87* 03(247) -> 248* s1(45) -> 46* s1(35) -> 36* s1(30) -> 31* s1(10) -> 11* s1(92) -> 93* s1(52) -> 53* s1(47) -> 48* s1(42) -> 43* s1(37) -> 38* s1(84) -> 85* s1(44) -> 45* s1(14) -> 15* s1(9) -> 10* s1(96) -> 97* s1(6) -> 7* s1(113) -> 114* s1(93) -> 94* s1(83) -> 84* s1(48) -> 49* s1(38) -> 39* s1(8) -> 9* s1(90) -> 91* s3(242) -> 243* s3(266) -> 267* s3(246) -> 247* s3(241) -> 242* s3(238) -> 239* s3(240) -> 241* p1(50) -> 51* p1(40) -> 41* p1(97) -> 98* p1(32) -> 33* p1(12) -> 13* p1(7) -> 8* p1(94) -> 95* p1(89) -> 90* p1(49) -> 50* p1(39) -> 40* p1(51) -> 52* p1(46) -> 47* p1(36) -> 37* p1(11) -> 12* p1(88) -> 89* p1(53) -> 54* p1(43) -> 44* p1(33) -> 34* p1(13) -> 14* p1(95) -> 96* p1(85) -> 86* p4(276) -> 277* p4(270) -> 271* foo1(91) -> 92* foo1(41) -> 42* bar1(34) -> 35* p2(182) -> 183* p2(172) -> 173* p2(137) -> 138* p2(127) -> 128* p2(117) -> 118* p2(219) -> 220* p2(174) -> 175* p2(139) -> 140* p2(134) -> 135* p2(124) -> 125* p2(221) -> 222* p2(141) -> 142* p2(131) -> 132* p2(121) -> 122* p2(188) -> 189* p2(138) -> 139* p2(128) -> 129* p2(220) -> 221* p2(215) -> 216* p2(200) -> 201* p2(190) -> 191* p2(180) -> 181* p2(120) -> 121* foo0(2) -> 3* foo0(1) -> 3* s2(222) -> 223* s2(217) -> 218* s2(132) -> 133* s2(214) -> 215* s2(119) -> 120* s2(251) -> 252* s2(216) -> 217* s2(136) -> 137* s2(126) -> 127* s2(116) -> 117* s2(268) -> 269* s2(218) -> 219* s2(133) -> 134* s2(123) -> 124* s2(118) -> 119* s2(140) -> 141* s2(135) -> 136* s2(130) -> 131* s2(125) -> 126* 00(2) -> 1* 00(1) -> 1* foo2(129) -> 130* s0(2) -> 2* s0(1) -> 2* bar2(122) -> 123* p0(2) -> 5* p0(1) -> 5* p3(264) -> 265* p3(244) -> 245* p3(239) -> 240* p3(204) -> 205* p3(194) -> 195* p3(236) -> 237* p3(206) -> 207* p3(243) -> 244* p3(245) -> 246* p3(210) -> 211* bar0(2) -> 4* bar0(1) -> 4* 1 -> 5,30 2 -> 5,6 6 -> 175,8 7 -> 83* 8 -> 183,34 9 -> 189,33,182 10 -> 12,188,32 16 -> 3* 30 -> 175,8 31 -> 7* 35 -> 37* 37 -> 123,125,205,173 38 -> 40,172 41 -> 35* 42 -> 44* 44 -> 201* 45 -> 47* 47 -> 191,51,200 48 -> 50,190 52 -> 54* 54 -> 3* 83 -> 89,174 84 -> 86,88 85 -> 113* 86 -> 214* 87 -> 123,125,205,35,37,41,4 90 -> 116* 92 -> 181* 93 -> 95,180 96 -> 98,4 98 -> 37,41,4 115 -> 5* 116 -> 118* 118 -> 207,122 119 -> 121,206 123 -> 125* 125 -> 205,129 126 -> 128,204 130 -> 132* 132 -> 211,140,142 133 -> 135* 135 -> 195,210 136 -> 138,194 140 -> 142,92 142 -> 92* 173 -> 41* 175 -> 90* 181 -> 96* 183 -> 14,34 189 -> 13* 191 -> 51* 195 -> 139* 201 -> 52* 205 -> 129* 207 -> 122* 211 -> 140,142,96 214 -> 216* 216 -> 265,222 217 -> 237,221,264 218 -> 220,236 223 -> 251,238 224 -> 130,132,140,181,98,37,123,129,42,44,52,3 237 -> 221* 238 -> 240* 240 -> 277,246 241 -> 271,245,276 242 -> 244,270 247 -> 268,266 248 -> 130,132,140,181,98,37,123,129 251 -> 216* 252 -> 215* 265 -> 222* 266 -> 240* 267 -> 239* 268 -> 216,265 269 -> 215* 271 -> 245* 277 -> 246* problem: Qed